0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 88 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 202 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 QDPSizeChangeProof (⇔, 0 ms)
↳25 YES
IN_ORDERD_IN_GA(tree(X1, void, X2), X3) → U8_GA(X1, X2, X3, in_orderA_in_ga(X2, X4))
IN_ORDERD_IN_GA(tree(X1, void, X2), X3) → IN_ORDERA_IN_GA(X2, X4)
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → U1_GA(X1, X2, X3, X4, in_orderA_in_ga(X2, X5))
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → IN_ORDERA_IN_GA(X2, X5)
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U3_GA(X1, X2, X3, X4, in_orderA_in_ga(X3, X6))
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → IN_ORDERA_IN_GA(X3, X6)
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U4_GA(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U4_GA(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U5_GA(X1, X2, X3, X4, appB_in_ggga(X5, X1, X6, X4))
U4_GA(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → APPB_IN_GGGA(X5, X1, X6, X4)
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGGA(X1, X2, X3, X4, X5, appB_in_ggga(X2, X3, X4, X5))
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPB_IN_GGGA(X2, X3, X4, X5)
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U9_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X3, X7))
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → IN_ORDERA_IN_GA(X3, X7)
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_in_ga(X3, X7))
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → U11_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X4, X8))
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → IN_ORDERA_IN_GA(X4, X8)
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_in_ga(X4, X8))
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → U13_GA(X1, X2, X3, X4, X5, X6, appB_in_ggga(X7, X2, X8, X9))
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → APPB_IN_GGGA(X7, X2, X8, X9)
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → U14_GA(X1, X2, X3, X4, X5, X6, appcB_in_ggga(X7, X2, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → U15_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X5, X10))
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → IN_ORDERA_IN_GA(X5, X10)
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_out_ga(X5, X10)) → U17_GA(X1, X2, X3, X4, X5, X6, appC_in_ggga(X9, X1, X10, X6))
U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_out_ga(X5, X10)) → APPC_IN_GGGA(X9, X1, X10, X6)
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGGA(X1, X2, X3, X4, X5, appC_in_ggga(X2, X3, X4, X5))
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_GGGA(X2, X3, X4, X5)
in_ordercA_in_ga(void, []) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U19_ga(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appcB_in_ggga(X5, X1, X6, X4))
appcB_in_ggga([], X1, X2, .(X1, X2)) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
IN_ORDERD_IN_GA(tree(X1, void, X2), X3) → U8_GA(X1, X2, X3, in_orderA_in_ga(X2, X4))
IN_ORDERD_IN_GA(tree(X1, void, X2), X3) → IN_ORDERA_IN_GA(X2, X4)
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → U1_GA(X1, X2, X3, X4, in_orderA_in_ga(X2, X5))
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → IN_ORDERA_IN_GA(X2, X5)
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U3_GA(X1, X2, X3, X4, in_orderA_in_ga(X3, X6))
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → IN_ORDERA_IN_GA(X3, X6)
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U4_GA(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U4_GA(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U5_GA(X1, X2, X3, X4, appB_in_ggga(X5, X1, X6, X4))
U4_GA(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → APPB_IN_GGGA(X5, X1, X6, X4)
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U6_GGGA(X1, X2, X3, X4, X5, appB_in_ggga(X2, X3, X4, X5))
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPB_IN_GGGA(X2, X3, X4, X5)
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U9_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X3, X7))
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → IN_ORDERA_IN_GA(X3, X7)
IN_ORDERD_IN_GA(tree(X1, tree(X2, X3, X4), X5), X6) → U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_in_ga(X3, X7))
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → U11_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X4, X8))
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → IN_ORDERA_IN_GA(X4, X8)
U10_GA(X1, X2, X3, X4, X5, X6, in_ordercA_out_ga(X3, X7)) → U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_in_ga(X4, X8))
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → U13_GA(X1, X2, X3, X4, X5, X6, appB_in_ggga(X7, X2, X8, X9))
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → APPB_IN_GGGA(X7, X2, X8, X9)
U12_GA(X1, X2, X3, X4, X5, X6, X7, in_ordercA_out_ga(X4, X8)) → U14_GA(X1, X2, X3, X4, X5, X6, appcB_in_ggga(X7, X2, X8, X9))
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → U15_GA(X1, X2, X3, X4, X5, X6, in_orderA_in_ga(X5, X10))
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → IN_ORDERA_IN_GA(X5, X10)
U14_GA(X1, X2, X3, X4, X5, X6, appcB_out_ggga(X7, X2, X8, X9)) → U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_in_ga(X5, X10))
U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_out_ga(X5, X10)) → U17_GA(X1, X2, X3, X4, X5, X6, appC_in_ggga(X9, X1, X10, X6))
U16_GA(X1, X2, X3, X4, X5, X6, X9, in_ordercA_out_ga(X5, X10)) → APPC_IN_GGGA(X9, X1, X10, X6)
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → U7_GGGA(X1, X2, X3, X4, X5, appC_in_ggga(X2, X3, X4, X5))
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_GGGA(X2, X3, X4, X5)
in_ordercA_in_ga(void, []) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U19_ga(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appcB_in_ggga(X5, X1, X6, X4))
appcB_in_ggga([], X1, X2, .(X1, X2)) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_GGGA(X2, X3, X4, X5)
in_ordercA_in_ga(void, []) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U19_ga(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appcB_in_ggga(X5, X1, X6, X4))
appcB_in_ggga([], X1, X2, .(X1, X2)) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
APPC_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPC_IN_GGGA(X2, X3, X4, X5)
APPC_IN_GGGA(.(X1, X2), X3, X4) → APPC_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPB_IN_GGGA(X2, X3, X4, X5)
in_ordercA_in_ga(void, []) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U19_ga(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appcB_in_ggga(X5, X1, X6, X4))
appcB_in_ggga([], X1, X2, .(X1, X2)) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
APPB_IN_GGGA(.(X1, X2), X3, X4, .(X1, X5)) → APPB_IN_GGGA(X2, X3, X4, X5)
APPB_IN_GGGA(.(X1, X2), X3, X4) → APPB_IN_GGGA(X2, X3, X4)
From the DPs we obtained the following set of size-change graphs:
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → U2_GA(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U2_GA(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → IN_ORDERA_IN_GA(X3, X6)
IN_ORDERA_IN_GA(tree(X1, X2, X3), X4) → IN_ORDERA_IN_GA(X2, X5)
in_ordercA_in_ga(void, []) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3), X4) → U19_ga(X1, X2, X3, X4, in_ordercA_in_ga(X2, X5))
U19_ga(X1, X2, X3, X4, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X4, X5, in_ordercA_in_ga(X3, X6))
U20_ga(X1, X2, X3, X4, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, X4, appcB_in_ggga(X5, X1, X6, X4))
appcB_in_ggga([], X1, X2, .(X1, X2)) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4, .(X1, X5)) → U22_ggga(X1, X2, X3, X4, X5, appcB_in_ggga(X2, X3, X4, X5))
U22_ggga(X1, X2, X3, X4, X5, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, X4, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
IN_ORDERA_IN_GA(tree(X1, X2, X3)) → U2_GA(X1, X2, X3, in_ordercA_in_ga(X2))
U2_GA(X1, X2, X3, in_ordercA_out_ga(X2, X5)) → IN_ORDERA_IN_GA(X3)
IN_ORDERA_IN_GA(tree(X1, X2, X3)) → IN_ORDERA_IN_GA(X2)
in_ordercA_in_ga(void) → in_ordercA_out_ga(void, [])
in_ordercA_in_ga(tree(X1, X2, X3)) → U19_ga(X1, X2, X3, in_ordercA_in_ga(X2))
U19_ga(X1, X2, X3, in_ordercA_out_ga(X2, X5)) → U20_ga(X1, X2, X3, X5, in_ordercA_in_ga(X3))
U20_ga(X1, X2, X3, X5, in_ordercA_out_ga(X3, X6)) → U21_ga(X1, X2, X3, appcB_in_ggga(X5, X1, X6))
appcB_in_ggga([], X1, X2) → appcB_out_ggga([], X1, X2, .(X1, X2))
appcB_in_ggga(.(X1, X2), X3, X4) → U22_ggga(X1, X2, X3, X4, appcB_in_ggga(X2, X3, X4))
U22_ggga(X1, X2, X3, X4, appcB_out_ggga(X2, X3, X4, X5)) → appcB_out_ggga(.(X1, X2), X3, X4, .(X1, X5))
U21_ga(X1, X2, X3, appcB_out_ggga(X5, X1, X6, X4)) → in_ordercA_out_ga(tree(X1, X2, X3), X4)
in_ordercA_in_ga(x0)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
appcB_in_ggga(x0, x1, x2)
U22_ggga(x0, x1, x2, x3, x4)
U21_ga(x0, x1, x2, x3)
From the DPs we obtained the following set of size-change graphs: